Corelab Seminar
2013-2014
Fotis Iliopoulos (NTUA)
Local Search Algorithms inspired by the Lovasz Local Lemma
Abstract.
For a CNF formula $F$ with $n$ variables, let $E: \{0,1\}^n \to \mathbf{N}$ be the (energy) function counting the number of
violated clauses at each value assignment. A number of practically useful satisfiability algorithms start at a random
$\sigma \in \{0,1\}^n$ and, while violated clauses exist, employ a randomized process to select a violated clause $c$
and new values for its variables, leading to a new state $\tau$. For both the choice of $c$ and the choice of values for
its variables there exists a cornucopia of heuristics, but not much to distinguish between them besides experiments, the
systematic conduct of which forms an entire subarea of satisfiability research. One property that is shared by the vast majority
of these heuristics is that they are primarily guided by the new number of violated clauses, $E(\tau)$, i.e., they largely focus
on the energetic potential near the current truth assignment $\sigma$.
Inspired by Moser's~\cite{moser} groundbreaking algorithmic argument for the Lov\'{a}sz Local Lemma we show that there is an
alternative \emph{entropic} potential to consider that lends itself to rigorous mathematical analysis. Focusing on this potential
suggests a systematic methodology for designing algorithms for any discrete-valued CSP, while also elucidating why certain
existing heuristics perform as well as they do. For example, our work suggests an explanation for the following, rather surprising,
experimental finding of Balint and Sch\"{o}ning~\cite{balint}: in choosing new values for $c$ one should focus on minimizing
the number of clauses that will become unsatisfied, ignoring the clauses that will become satisfied. We also derive new positive
algorithmic results, in the style of the Lov\'{a}sz Local Lemma, for formulas in which clauses share multiple variables or have
local neighborhoods that are not locally tree-like.